Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(nil,k)	→ k
2:		app(l,nil)	→ l
3:		app(cons(x,l),k)	→ cons(x,app(l,k))
4:		sum(cons(x,nil))	→ cons(x,nil)
5:		sum(cons(x,cons(y,l)))	→ sum(cons(plus(x,y),l))
6:		sum(app(l,cons(x,cons(y,k))))	→ sum(app(l,sum(cons(x,cons(y,k)))))
7:		plus(0,y)	→ y
8:		plus(s(x),y)	→ s(plus(x,y))
9:		sum(plus(cons(0,x),cons(y,l)))	→ pred(sum(cons(s(x),cons(y,l))))
10:		pred(cons(s(x),nil))	→ cons(x,nil)

There are 9 dependency pairs:


11:		APP(cons(x,l),k)	→ APP(l,k)
12:		SUM(cons(x,cons(y,l)))	→ SUM(cons(plus(x,y),l))
13:		SUM(cons(x,cons(y,l)))	→ PLUS(x,y)
14:		SUM(app(l,cons(x,cons(y,k))))	→ SUM(app(l,sum(cons(x,cons(y,k)))))
15:		SUM(app(l,cons(x,cons(y,k))))	→ APP(l,sum(cons(x,cons(y,k))))
16:		SUM(app(l,cons(x,cons(y,k))))	→ SUM(cons(x,cons(y,k)))
17:		PLUS(s(x),y)	→ PLUS(x,y)
18:		SUM(plus(cons(0,x),cons(y,l)))	→ PRED(sum(cons(s(x),cons(y,l))))
19:		SUM(plus(cons(0,x),cons(y,l)))	→ SUM(cons(s(x),cons(y,l)))

The approximated dependency graph contains 4 SCCs: {11}, {17}, {12} and {14}.

Consider the SCC {11}. There are no usable rules. By taking the AF π with π(APP) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 11 is strictly decreasing.

Consider the SCC {17}. There are no usable rules. By taking the AF π with π(PLUS) = 1 together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Consider the SCC {12}. The usable rules are {7,8}. By taking the AF π with π(s) = π(SUM) = 1, π(plus) = 2 and π(cons) = [2] together with the lexicographic path order with empty precedence, the rules in {7,8} are weakly decreasing and rule 12 is strictly decreasing.

Consider the SCC {14}. The constraints could not be solved.

Tyrolean Termination Tool (5.32 seconds) --- May 4, 2006